COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 lispax.lsp[w82,jmc] ekl axioms for lisp with infixes
C00025 ENDMK
C⊗;
;;; lispax.lsp[w82,jmc] ekl axioms for lisp with infixes
;;; These axioms require a file EKL.INI in the user's area containing the
;;; definition 
;;;
;;; (defun lname fexpr (x)
;;;        ((lambda (careful)
;;; 		(mapc (function
;;; 		       (lambda (y)
;;; 			       (apply 'linename
;;; 				      (cond ((assq y g:linenames)
;;; 					     (list y y -1))
;;; 					    (t (list y -1))))))
;;; 		      x))
;;;	     nil))
;;;
;;; The file LNAME.LSP[EKL,JJW] contains this definition; also ekl.ini[w82,jmc].
;;; This function  lname  is used to collect axioms into the groups
;;; DEFINFO containing recursive function definitions,
;;; SIMPINFO used for simplifying, and
;;; SORTINFO used for determining the sorts expressions for lambda conversion.
;;; etc.

(wipe-out)

(proof lispax)

(DECL (U u0 u1 u2 u3 v v0 v1 v2 v3 W w0 w1 w2 w3) |ground| variable listp)

(DECL (X Y Z) |GROUND| VARIABLE sEXP)

(decl (xa ya za) |ground| variable atom)

(DECL (A B C) |GROUND| VARIABLE)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(DECL (NNIL) |GROUND| CONsTANT LIsTp)

(DECL (CONs) |GROUND⊗GROUND→GROUND| CONsTANT)

(DECL (~) |GROUND⊗GROUND→GROUND| CONsTANT NIL INFIX 850)

(DECL (CAR CDR) |GROUND→GROUND| CONsTANT nil unary 950)

(DECL (ATOM NULL) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(DECL (LIsTp) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(DECL (sEXP) |GROUND→TRUTHVAL| CONsTANT nil unary 750)

(AXIOM |∀U.sEXP U |)
(lname sortinfo)

(AXIOM |∀X U.LISTP X~U |)
(lname sortinfo simpinfo)

(AXIOM |∀U.NULL U ≡ U=NNIL|)
(lname nilprop)
(axiom |atom nnil|)
(lname nilprop)
(axiom |∀u.atom u ⊃ u=nnil|)
(lname nilprop)

(axiom |null nnil|)
(lname simpinfo nilprop)

(AXIOM |∀X Y.SEXP X~Y|)
(lname sortinfo)

(AXIOM |∀X Y.¬ATOM X~Y|)
(lname consfacts simpinfo)

(AXIOM |∀X U.¬NULL X~U|)
(lname consfacts simpinfo)

(AXIOM |∀X U.CAR (X ~ U) = X|)
(lname simpinfo)

(AXIOM |∀X U.CDR (X~U) = U|)
(lname simpinfo)

(AXIOM |∀X Y.CAR (X ~ Y) = X|)
(lname consfacts simpinfo)

(AXIOM |∀X Y.CDR (X~Y) = Y|)
(lname consfacts simpinfo)

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(X~U))⊃(∀U.PHI(U))|)
(lname listinduction)

(AXIOM |∀PHI.(∀X.ATOM X ⊃ PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X~Y))⊃(∀X.PHI(X))|)
(lname sexpinduction)

;;; Lists of variable numbers of arguments require special treatment.

(decl list |ground* → ground| functional)

(axiom |∀x.listp(list(x))|)
(lname sortinfo)

(axiom |∀x.list(x) = x~nnil|)
(lname simpinfo)

(axiom |∀x y.listp(list(x,y))|)
(lname sortinfo)

(axiom |∀x y.list(x,y) = x~list(y)|)
(lname simpinfo)

(axiom |∀x y z.listp(list(x,y,z))|)
(lname sortinfo)

(axiom |∀x y z.list(x,y,z) = x~list(y,z)|)
(lname simpinfo)

;;; some defined functions and theorems taken as axioms


(DECL (*) |GROUND⊗ground*→GROUND| functional NIL INFIX 840 both)
;;; This is LISP's append.  While it can be proved associative, it
;;; is convenient in proofs of other theorems to have it declared
;;; associative.

(axiom |∀u v.listp(u*v)|)
(lname sortinfo listappend)

(AXIOM |∀U V.(U*V)=IF NULL(U) THEN V ELsE CAR U ~ (CDR U *V)|)
(lname definfo)

(axiom |∀u.nnil*u=u|)
(lname appendfacts simpinfo)

(axiom |∀x u v.x~u*v = x~(u*v)|)
(lname appendfacts simpinfo)

;;; (axiom |∀u v w.(u*v)*w = u*(v*w)|)
;;; (lname assocappend)
;;; not needed any more

(decl (alist a0 a1 a2) ground variable alistp)
(axiom |∀alist. listp alist|)
(lname simpinfo sortinfo)
(axiom |∀alist. ¬null alist ⊃ ¬atom car alist ∧ atom car car alist|)

(axiom |∀xa y alist.alistp ((xa ~ y) ~ alist)|)
(lname mkalist)

(decl assoc |ground⊗ground → ground| constant)

(axiom |∀x alist. assoc(x,alist) =
                       if null alist then nnil
                       else if x = car car alist then car alist
                       else assoc(x, cdr alist)|)
(lname definfo)

(axiom |∀x alist.sexp assoc(x,alist)|)
(lname sortinfo)

(decl member |ground⊗ground → truthval| constant)

(axiom |∀x u. member(x,u) ≡ ¬null u ∧ (x = car u ∨ member(x, cdr u))|)
(lname definfo)

(decl (reverse) |ground→ground| constant nil unary 950)

(axiom |∀u.listp(reverse(u))|)
(lname sortinfo)

(axiom |∀u.reverse(u) = if null(u) then nnil
                        else reverse(cdr u) * list(car u)|)
(lname definfo)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)
(lname reverseappend)

(axiom |∀u.reverse(reverse(u)) = u|)
(lname reversereverse)

(decl subst |ground⊗ground⊗ground → ground| constant)
(axiom |∀x y z.subst(x,y,z) = if atom z then (if z = y then x else z)
                              else subst(x,y,car z)~subst(x,y,cdr z)|)
(lname definfo)